#include <vector>
#include <utility>
#include <stdexcept>
#include <algorithm>
#include <set>
#include "Generators.h"
#include "2SAT.h"

HashLexem generateHashLexem(int argumentsNum){
	HashLexem generatedLexem;
	generatedLexem.firstHash = generateNumberMod(argumentsNum);
	generatedLexem.secondHash = generateNumberMod(argumentsNum);
	generatedLexem.isTrueFirst = rand() % 2;
	generatedLexem.isTrueSecond = rand() % 2;
	return generatedLexem;
}

void stressCheckUnsolvableSolution(){
	for (int numberTest = 0; numberTest < 100; ++numberTest){
		std::cout << numberTest << std::endl;
		int argumentsNum = std::max<int>(getRandomPositiveNumber() % 10000, 1);
		std::vector<int> cycle = generateCycle(argumentsNum);
		std::vector<HashLexem> inputHashLexems;
		std::cerr << "TEST:" << std::endl;
		std::cerr << numberTest << std::endl;
		std::cerr << cycle.size() << std::endl;
		for (size_t numInCycle = 0; numInCycle < cycle.size(); ++numInCycle){
			HashLexem currentLexem;
			currentLexem.firstHash = cycle[numInCycle];
			currentLexem.secondHash = cycle[(numInCycle + 1) % cycle.size()];
			currentLexem.isTrueFirst = true;
			currentLexem.isTrueSecond = false;
			inputHashLexems.push_back(currentLexem);
		}
		HashLexem badHash;
		badHash.firstHash = cycle[generateNumberMod(cycle.size())];
		badHash.secondHash = cycle[generateNumberMod(cycle.size())];
		badHash.isTrueFirst = true;
		badHash.isTrueSecond = true;
		HashLexem badHash2;
		badHash2.firstHash = cycle[generateNumberMod(cycle.size())];
		badHash2.secondHash = cycle[generateNumberMod(cycle.size())];
		badHash2.isTrueFirst = false;
		badHash2.isTrueSecond = false;
		//std::cerr << "BAD HASH" << std::endl;
		inputHashLexems.push_back(badHash);
		inputHashLexems.push_back(badHash2);
		int additionalHashNumbers = generateNumberMod(argumentsNum * 3);
		for (int numberAddHash = 0; numberAddHash < additionalHashNumbers; ++numberAddHash){
			inputHashLexems.push_back(generateHashLexem(argumentsNum));
		}
		std::vector<bool> solutionArguments;
		if (satFindingHashSolutions(argumentsNum, inputHashLexems, solutionArguments)){
			throw std::logic_error("Found extra solution");
		}
	}
}

void check2SatSolution(const std::vector<HashLexem>& listOfHashedLexems, const std::vector<bool>& solution){
	for (auto currentLexem : listOfHashedLexems){
		bool lexem1 = solution[currentLexem.firstHash];
		if (!currentLexem.isTrueFirst)
			lexem1 = (!lexem1);
		bool lexem2 = solution[currentLexem.secondHash];
		if (!currentLexem.isTrueSecond)
			lexem2 = (!lexem2);
		bool resultLexem = (lexem1 | lexem2);
		//std::cout << resultLexem << std::endl;
		if (!resultLexem){
			throw std::logic_error("Wrong answer on 2SAT answer!");
		}
	}
}

void generate2SatSolvableExpression(int& argumentsNum, std::vector<HashLexem>& inputHashes){
	argumentsNum = std::max<int>(getRandomPositiveNumber() % 20000, 1);
	std::vector<bool> bitMaskOfAnswer(argumentsNum);
	for (size_t currentBitNumber = 0; currentBitNumber < bitMaskOfAnswer.size(); ++currentBitNumber){
		bitMaskOfAnswer[currentBitNumber] = rand() % 2;
	}
	int numberOfExpressions = std::min<int>(std::max<int>(getRandomPositiveNumber() % 200000, 1), 10 * argumentsNum);
	for (int currentExpressionNum = 0; currentExpressionNum < numberOfExpressions; ++currentExpressionNum){
		HashLexem currentLexem;
		std::pair<int, int> currentPairOfArguments = getRandomNumbers(argumentsNum);
		currentLexem.firstHash = currentPairOfArguments.first;
		currentLexem.secondHash = currentPairOfArguments.second;
		if (!bitMaskOfAnswer[currentPairOfArguments.first]){
			currentLexem.isTrueFirst = false;
		}
		else{
			currentLexem.isTrueFirst = true;
		}
		currentLexem.isTrueSecond = rand() % 2;
		inputHashes.push_back(currentLexem);
	}
}

void stressCheckSolvableSolution(){
	for (int testNumber = 0; testNumber < 100; ++testNumber){
		std::cout << testNumber << std::endl;
		int argumentsNum;
		std::vector<HashLexem> inputHashLexems;
		generate2SatSolvableExpression(argumentsNum, inputHashLexems);
		std::vector<bool> solutionArguments;
		bool existsSolution = satFindingHashSolutions(argumentsNum, inputHashLexems, solutionArguments);
		if (!existsSolution){
			throw std::logic_error("Solution exists!");
		}
		check2SatSolution(inputHashLexems, solutionArguments);
	}
}

void generate2SatExpression(int& argumentsNum, std::vector<HashLexem>& inputExpressions){
	argumentsNum = std::max<int>(getRandomPositiveNumber() % 1000, 1);
	int expressionNumbers = std::max<int>(getRandomPositiveNumber() % 10000, argumentsNum * 10);
	for (int currentExpressionNumber = 0; currentExpressionNumber < expressionNumbers; ++currentExpressionNumber){
		HashLexem currentExpression = generateHashLexem(argumentsNum);
		inputExpressions.push_back(currentExpression);
	}
}

void stress2SatGraph(){
	for (int testNumber = 0; testNumber < 100; ++testNumber){
		std::cout << testNumber << std::endl;
		int argumentsNum;
		std::vector<HashLexem> expressions;
		generate2SatExpression(argumentsNum, expressions);
		
		std::unique_ptr<Graph> G = buildSatGraph(expressions, argumentsNum);
		std::set<Edge> edgesList;
		for (auto currentExpression : expressions){
			int fromVertex, toVertex;
			fromVertex = currentExpression.firstHash * 2;
			if (currentExpression.isTrueFirst)
				fromVertex++;
			toVertex = currentExpression.secondHash * 2;
			if (!currentExpression.isTrueSecond)
				++toVertex;
			edgesList.insert({ fromVertex, toVertex });
			fromVertex = currentExpression.secondHash * 2;
			if (currentExpression.isTrueSecond)
				++fromVertex;
			toVertex = currentExpression.firstHash * 2;
			if (!currentExpression.isTrueFirst)
				++toVertex;
			edgesList.insert({ fromVertex, toVertex });
		}
		std::set<Edge> edgesGraphList;
		for (int currentVertex = 0; currentVertex < G->getVertexNum(); ++currentVertex){
			std::vector<int> adjacentList = G->getAdjacentList(currentVertex);
			for (auto toVertex : adjacentList){
				edgesGraphList.insert({ currentVertex, toVertex });
			}
		}
		for (auto currentEdge : edgesList){
			if (edgesGraphList.count(currentEdge) == 0){
				throw std::logic_error("Our list is bigger than edges on graph");
			}
		}
		for (auto currentEdge : edgesGraphList){
			if (edgesList.count(currentEdge) == 0){
				throw std::logic_error("There are extra vertexes in graph");
			}
		}
	}
}
